Problem:
 d(x) -> e(u(x))
 d(u(x)) -> c(x)
 c(u(x)) -> b(x)
 v(e(x)) -> x
 b(u(x)) -> a(e(x))

Proof:
 Bounds Processor:
  bound: 1
  enrichment: match
  automaton:
   final states: {7,6,5,4}
   transitions:
    a1(47) -> 48*
    e1(54) -> 55*
    e1(9) -> 10*
    e1(56) -> 57*
    e1(46) -> 47*
    b1(40) -> 41*
    b1(42) -> 43*
    b1(34) -> 35*
    c1(32) -> 33*
    c1(24) -> 25*
    c1(26) -> 27*
    u1(16) -> 17*
    u1(18) -> 19*
    u1(8) -> 9*
    d0(2) -> 4*
    d0(1) -> 4*
    d0(3) -> 4*
    e0(2) -> 1*
    e0(1) -> 1*
    e0(3) -> 1*
    u0(2) -> 2*
    u0(1) -> 2*
    u0(3) -> 2*
    c0(2) -> 5*
    c0(1) -> 5*
    c0(3) -> 5*
    b0(2) -> 7*
    b0(1) -> 7*
    b0(3) -> 7*
    v0(2) -> 6*
    v0(1) -> 6*
    v0(3) -> 6*
    a0(2) -> 3*
    a0(1) -> 3*
    a0(3) -> 3*
    1 -> 54,6,40,26,16
    2 -> 46,6,34,24,18
    3 -> 56,6,42,32,8
    10 -> 4*
    17 -> 9*
    19 -> 9*
    25 -> 4*
    27 -> 4*
    33 -> 4*
    35 -> 25,4,5
    41 -> 25,4,5
    43 -> 25,4,5
    48 -> 35,5,7
    55 -> 47*
    57 -> 47*
  problem:
   
  Qed